package component;

import java.util.ArrayList;

import Prism.core.AbstractImplementation;
import Prism.core.Event;
import Prism.core.PrismConstants;

public class NossDatabase extends AbstractImplementation {
	// prov Name(Event Name)
	public static final String provGetPhoneNumbers = "getPhoneNumbers";
	public static final String provAddPhoneNumber = "addPhoneNumber";
	public static final String provDeletePhoneNumber = "deletePhoneNumber";
	
	// usedPhoneNumbers: \set PhoneNumber;
	ArrayList<String> usedPhoneNumbers;
	
	// Check invariant property
	public boolean checkInvariant() {
		//#usedPhoneNumber \eqgreater 0;
		if(usedPhoneNumbers.size()>=0) return true;
		return false;
	}
	
	@Override
	public void start() {
		super.start();
		usedPhoneNumbers = new ArrayList<String>();
		
		// Test Phone Number
		usedPhoneNumbers.add("2132548799");
		usedPhoneNumbers.add("1231231231");
		usedPhoneNumbers.add("2342342342");
		usedPhoneNumbers.add("3453453453");
	}
	
	@Override
	public void handle(Event e) {
		// Handle of request of provGetPhoneNumbers
		if(e.getName().equals(provGetPhoneNumbers)) {
			// pre #list = 0;
			// post (#~list \eqgreater 0) \and (\result = list);
			if(checkInvariant()) {
				Event n;
				
				int size = usedPhoneNumbers.size();
				for(int i=0; i<size; i++) {
					n = new Event(provGetPhoneNumbers, PrismConstants.REPLY);
					n.addParameter("phoneNumber", (String)usedPhoneNumbers.get(i));
					n.addParameter("clearFlag", (i==0)?"true":"false");
					this.send(n);
				}
			}
			
		}
		// Handle of request of provAddPhoneNumber
		else if(e.getName().equals(provAddPhoneNumber)) {
			// pre id \not_in usedPhoneNumbers;
			if(usedPhoneNumbers.contains((String)e.getParameter("phoneNumber"))==false) {
				// post (#~usedPhoneNumbers=#usedPhoneNumbers+1)
				// \and (id \in usedPhoneNumbers);
				usedPhoneNumbers.add((String)e.getParameter("phoneNumber"));
			}
		}
		else if(e.getName().equals(provDeletePhoneNumber)) {
			// pre id \in usedPhoneNumbers; 
			if(usedPhoneNumbers.contains((String)e.getParameter("phoneNumber"))) {
				// post (#~usedPhoneNumbers=#usedPhoneNumbers-1)
				// \and (id \not_in usedPhoneNumbers);
				usedPhoneNumbers.remove((String)e.getParameter("phoneNumber"));
			}
		}
	}
}
